package stackSample;
import gov.nasa.jpf.jvm.MJIEnv;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.lang.reflect.Method;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

public class JPF_stackSample_InterfaceGenerator {

	static Set<State> states = new HashSet<State>();
	static Map<State, Set<State>> fsm = new HashMap<State, Set<State>>();

	public static boolean updateFSM(MJIEnv env, int objref, int intArrRefPre, int intArrRefPost) {
		State preState = (State) addStateIfNeeded(env, intArrRefPre)[0];

		Object[] tmp = addStateIfNeeded(env, intArrRefPost);
		State postState = (State) tmp[0];

		// if needed, create map to store transitions from pre-state 
		Set<State> edges = fsm.get(preState);
		if (edges == null) {
			edges = new HashSet<State>();
			fsm.put(preState, edges);
		}

		// add post state to transition set 
		edges.add(postState);
		return ((Boolean) tmp[1]).booleanValue();
	}

	private static Object[] addStateIfNeeded(MJIEnv env, int intArrRef) {

		int[] opts = env.getIntArrayObject(intArrRef);
		State state = new State(Stack.class,opts);//TODO pass Class as parameter

		boolean isNew = states.add(state);

		return new Object[]{state, isNew};
	}

	public static void dumpFSM() {

//		for (Map.Entry<State, Set<State>> entry: fsm.entrySet()) {
//			State preState = entry.getKey();
//			System.out.println(preState + ":" + entry.getValue());			
//		}

		generateGrath();
	}

	private static void generateGrath(){

		StringBuffer sb = new StringBuffer();		
		Map<State,Integer> tmp = new HashMap<State,Integer>();
		Class cls = null;
		int index = 1;

		// Nodes
		sb.append("\ndigraph enabledness {\n");
		for (State state : states) {
			sb.append(index);
			sb.append(" [label=\"");
			sb.append(index);
			sb.append("\"]\n");
			tmp.put(state, index);
			index++;
			cls = state.getStateClass();
		}
		sb.append("\n");

		// Edges
		for (Map.Entry<State, Set<State>> entry: fsm.entrySet()) {

			State preState = entry.getKey();
			Set<State> postStates = entry.getValue();

			for (State postState : postStates) {

				int preIndex = tmp.get(preState);
				int postIndex = tmp.get(postState);
				Method[] methods = postState.getEnabledMethods();
				
				sb.append(preIndex);
				sb.append("->");
				sb.append(postIndex);
				sb.append(" [label=\"<");

				for (int i = 0; i < methods.length; i++) {					
					sb.append(methods[i].getName());
					if((i+1) < methods.length)
						sb.append(" | ");
				}
				
				sb.append(">\"]\n");

			}

		}
		sb.append("}");
		
		//saving .dot file and generating .png graph
		String fileName = cls.getName() + ".dot";
		try{
			File myFile = new File(fileName);
			myFile.delete();
			
			BufferedWriter writer = new BufferedWriter(new FileWriter(fileName,true));
			writer.write(sb.toString());
			writer.flush();
			writer.close();
			Runtime.getRuntime().exec("dot -Tpng -o"+ cls.getName() + ".png " + fileName);
		}catch(Exception e){

		}

	}

}